mcsta

Benchmark
Model:coupon v.1 (DTMC)
Parameter(s)N = 9, DRAWS = 4, B = 5
Property:collect_all_bounded (prob-reach-reward-bounded)
Invocation (default)
mcsta/modest mcsta coupon.9-4.jani -E B=5 --props collect_all_bounded -O out.txt Minimal --unsafe --es -S Memory --reward-bounded-alg StateElimination
Execution
Walltime:78.33459496498108s
Return code:0
Relative Error:0.4483422481623962
Log
coupon.9-4.jani:model: info: coupon.9-4 is a DTMC model.
coupon.9-4.jani: info: Need 16 bytes per state.
coupon.9-4.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
coupon.9-4.jani: info: Explored 21077063 states for B=5.

Peak memory usage: 5451 MB
Analysis results for coupon.9-4.jani
Experiment B=5

+ State space exploration
  State size:  16 bytes
  States:      21077063
  Transitions: 21077063
  Branches:    24429223
  Rate:        1052537 states/s
  Time:        21.8 s

+ Property collect_all_bounded
  Probability: 0.1977752563227128
  Bounds:      [0.1977752563227128, 0.1977752563227128]
  CDF:         { (0, 0), ..., (2, 0), (3, 0.028620066090515834), (4, 0.13211546740874242), (5, 0.1977752563227128) }
  Time:        55.9 s

  + Essential states
    Iterations:       4
    Essential states: 3771692
    Transitions:      3771692
    Branches:         7123852
    Time:             3.4 s

  + State elimination
    States:      514
    Transitions: 514
    Branches:    113539
    Time:        52.4 s

  + Value iteration
    Time: 0.0 s

Exported results to file "/out.txt".
STDERR
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.